PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 23:50:57 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -e 5e-2 -heuristic speed -ddextraactionvars 100 -maxiters 1000000 wlan.4.prism wlan.props --property cost_min -const COL=0
Parsing model file "wlan.4.prism"...
Type: MDP
Modules: medium station1 station2
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Parsing properties file "wlan.props"...
7 properties:
(1) "collisions": Pmax=? [ F col=COL ]
(2) "cost_max": R{"cost"}max=? [ F s1=12&s2=12 ]
(3) "cost_min": R{"cost"}min=? [ F s1=12&s2=12 ]
(4) "num_collisions": R{"collisions"}max=? [ F s1=12&s2=12 ]
(5) "sent": P>=1 [ F s1=12&s2=12 ]
(6) "time_max": R{"time"}max=? [ F s1=12&s2=12 ]
(7) "time_min": R{"time"}min=? [ F s1=12&s2=12 ]
---------------------------------------------------------------------
Model checking: "cost_min": R{"cost"}min=? [ F s1=12&s2=12 ]
Model constants: COL=0
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Warning: Switching to explicit engine to allow interval iteration on Rmin operator.
Building model...
Model constants: COL=0
Computing reachable states... 242859 345000 states
Reachable states exploration and model construction done in 3.708 secs.
Sorting reachable states list...
Time for model construction: 4.478 seconds.
Type: MDP
States: 345000 (1 initial)
Transitions: 762252
Choices: 440206
Max/avg: 3/1.28
Building reward structure...
Starting expected reachability (min)...
Starting Prob1 (max)...
Prob1 (max) took 797 iterations and 10.552 seconds.
target=1, inf=0, rest=344999
For Rmin, checking for zero-reward ECs...
Time for checking for zero-reward ECs: 0.267 seconds, no zero-reward ECs found, proceeding normally.
Computing upper bound(s) for Rmin using the Dijkstra Sweep for Monotone Pessimistic Initialization algorithm...
Calculating incoming choices relation for Markov decision process... done (0.113 seconds)
Time for computing upper bound(s) for Rmin using the DSI-MP algorithm: 1.34 seconds.
Upper bound for min expectation (Dijkstra Sweep MPI): 416071.75369262695
Starting Prob1 (min)...
Prob1 (min) took 854 iterations and 11.007 seconds.
Relevant sub-MDP is contracting, proceed...
Starting interval iteration (min, with Power method)...
Iteration 104: max relative diff=243.748090407, 5.05 sec so far
Iteration 209: max relative diff=119.600508317, 10.08 sec so far
Iteration 313: max relative diff=79.790631785, 15.07 sec so far
Iteration 418: max relative diff=59.3002541584, 20.08 sec so far
Iteration 523: max relative diff=47.1007807737, 25.08 sec so far
Iteration 628: max relative diff=39.0068993935, 30.11 sec so far
Iteration 733: max relative diff=33.2445887813, 35.12 sec so far
Max relative diff between upper and lower bound on convergence: 0.00769776498059
Interval iteration (min, with Power method) took 804 iterations, 1225699608 multiplications and 38.592 seconds.
Maximum finite value in solution vector at end of interval iteration: 415988.96713256836
Expected reachability took 61.842 seconds.
Value in the initial state: 7625.0
Time for model checking: 62.404 seconds.
Result: 7625.0 (value in the initial state)
Overall running time: 67.522 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.